definitionally equal

実際、Leanのカーネルは (fun x => t) s と t[s/x](項 t の中の全ての x を s で置き換えた項) をdefinitionally equalとみなすのと同様に、任意の p : Prop に対して任意の2つの項 t1 t2 : p をdefinitionally equalとみなす。t1 t2 : p をdefinitionally equalとみなすことはproof irrelevance(証明無関係)と呼ばれ、前段落の解釈と矛盾しない。つまり、証明 t : p は依存型理論の言語の中で普通の項として扱うことができるが、t は p が真であるという事実以上の情報は持っていないということである。

ref: https://aconite-ac.github.io/theorem_proving_in_lean4_ja/propositions_and_proofs.html

これらの項がどのように評価されているのかは後ほど学ぶ。今のところ、次の依存型理論の重要な特徴に注目してほしい: 全ての項が計算上の動作を持ち、またnormalization(正規化)の概念をサポートしている。原則として、同じ値に簡約される2つの項はdefinitionally equalであると呼ばれる。Leanの型チェッカーはdefinitionally equalである2つの項を「同じ」とみなす。Leanは2つの項の間の相等関係を認識しサポートするために最善を尽くす。

ref: Function Abstraction and Evaluation (関数抽象と評価) | 依存型理論 - Theorem Proving in Lean 4 日本語訳

確認用

Q. definitionally equal